00100	COMMENT - These are the usual reflexivity, symmetry, and
00200	transitivity axioms for the equality of terms in the logic.
00300	Most likely, they are unnecessary since the replacement rule
00400	of inference is probably strong enough to do their work.
00500	Certainly, the other two can be proved from reflexivity.
00600	The definition of  is also given.;
00800	
00900	GIVEAX(REFLEX,(∀ X)(X=X));
01000	
01100	GIVEAX(SYMEQ,(∀ X)(∀ Y)(X=Y ⊃ Y=X));
01200	
01300	GIVEAX(TRANSEQ,(∀ X)(∀ Y)(∀ Z)(X=Y∧Y=Z ⊃ X=Z));
01400	
01500	GIVEAX(NOTEQ,(∀ X)(∀ Y)(X≠Y≡¬(X=Y)));
     

00100	END;